1 /-
2 Copyright (c) 2018 Kenny Lau. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Kenny Lau
5
6 The perfect closure of a field.
7 -/
8
9 import algebra.char_p
src └────────────┘
10
11 universes u v
12
13 /-- A perfect field is a field of characteristic p that has p-th root. -/
14 class perfect_field (α : Type u) [field α] (p : ℕ) [char_p α p] : Type u :=
id └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴
src └───┘ ┴ └────┘
typ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘
15 (pth_root : α → α)
id ┴ ┴ ┴
typ ┴ ┴ ┴
16 (frobenius_pth_root : ∀ x, frobenius α p (pth_root x) = x)
id ┴ └───────┘ ┴ ┴ └──────┘ ┴ ┴ ┴
src └───────┘ ┴
typ ┴ └───────┘ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └───────┘
17
18 theorem frobenius_pth_root (α : Type u) [field α] (p : ℕ) [char_p α p] [perfect_field α p] (x : α) :
id └───┘ ┴ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───┘ ┴ └────┘ └───────────┘
typ └───┘ ┴ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └────┘ └───────────┘
19 frobenius α p (perfect_field.pth_root p x) = x :=
id └───────┘ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴
src └───────┘ └────────────────────┘ ┴
typ └───────┘ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴
doc └───────┘
20 perfect_field.frobenius_pth_root p x
id └──────────────────────────────┘ ┴ ┴
src └──────────────────────────────┘
typ └──────────────────────────────┘ ┴ ┴
21
22 theorem pth_root_frobenius (α : Type u) [field α] (p : ℕ) [nat.prime p] [char_p α p] [perfect_field α p] (x : α) :
id └───┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───┘ ┴ └───────┘ └────┘ └───────────┘
typ └───┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────┘ └────┘ └───────────┘
23 perfect_field.pth_root p (frobenius α p x) = x :=
id └────────────────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘ └───────┘ ┴
typ └────────────────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
24 frobenius_inj α p _ _ (by rw frobenius_pth_root)
id └───────────┘ ┴ ┴ └────────────────┘
src └───────────┘ └─┘└────────────────┘
typ └───────────┘ ┴ ┴ └─┘└────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └────────────────────┘
25
26 instance pth_root.is_ring_hom (α : Type u) [field α] (p : ℕ) [nat.prime p] [char_p α p] [perfect_field α p] :
id └───┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴
src └───┘ ┴ └───────┘ └────┘ └───────────┘
typ └───┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────┘ └────┘ └───────────┘
27 is_ring_hom (@perfect_field.pth_root α _ p _ _) :=
id └─────────┘ └────────────────────┘ ┴ ┴
src └─────────┘ └────────────────────┘
typ └─────────┘ └────────────────────┘ ┴ ┴
doc └─────────┘
28 { map_one := frobenius_inj α p _ _ (by rw [frobenius_pth_root, frobenius_one]),
id └───────────┘ ┴ ┴ └────────────────┘ └───────────┘
src └───────────┘ └──┘└────────────────┘└┘└───────────┘┴
typ └───────────┘ ┴ ┴ └──┘└────────────────┘└┘└───────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └─────────────────────┘└─────────────┘┴
29 map_mul := λ x y, frobenius_inj α p _ _ (by simp only [frobenius_pth_root, frobenius_mul]),
id ┴ ┴ └───────────┘ ┴ ┴ └────────────────┘ └───────────┘
src └───────────┘ └─────────┘└────────────────┘└┘└───────────┘┴
typ ┴ ┴ └───────────┘ ┴ ┴ └─────────┘└────────────────┘└┘└───────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────────────────────────────┘
30 map_add := λ x y, frobenius_inj α p _ _ (by simp only [frobenius_pth_root, frobenius_add]) }
id ┴ ┴ └───────────┘ ┴ ┴ └────────────────┘ └───────────┘
src └───────────┘ └─────────┘└────────────────┘└┘└───────────┘┴
typ ┴ ┴ └───────────┘ ┴ ┴ └─────────┘└────────────────┘└┘└───────────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────────────────────────────┘
31
32 theorem is_ring_hom.pth_root {α : Type u} [field α] (p : ℕ) [nat.prime p] [char_p α p] [perfect_field α p]
id └───┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴
src └───┘ ┴ └───────┘ └────┘ └───────────┘
typ └───┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └───────┘ └────┘ └───────────┘
33 {β : Type v} [field β] [char_p β p] [perfect_field β p] (f : α → β) [is_ring_hom f] {x : α} :
id └───┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
src └───┘ └────┘ └───────────┘ └─────────┘
typ └───┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴
doc └────┘ └───────────┘ └─────────┘
34 f (perfect_field.pth_root p x) = perfect_field.pth_root p (f x) :=
id ┴ └────────────────────┘ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴
src └────────────────────┘ ┴ └────────────────────┘
typ ┴ └────────────────────┘ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴
35 frobenius_inj β p _ _ (by rw [← is_monoid_hom.map_frobenius f, frobenius_pth_root, frobenius_pth_root])
id └───────────┘ ┴ ┴ └─────────────────────────┘ ┴ └────────────────┘ └────────────────┘
src └───────────┘ └────┘└─────────────────────────┘┴ └┘└────────────────┘└┘└────────────────┘┴
typ └───────────┘ ┴ ┴ └────┘└─────────────────────────┘┴┴└┘└────────────────┘└┘└────────────────┘┴
doc └────┘ ┴ └┘ └┘ ┴
txt └────┘ ┴ └┘ └┘ ┴
par └────┘ ┴ └┘ └┘ ┴
pid └──┘ ┴ └┘ └┘ ┴
st └──────────────────────────────────┘└──────────────────┘└──────────────────┘┴
36
37 inductive perfect_closure.r (α : Type u) [monoid α] (p : ℕ) : (ℕ × α) → (ℕ × α) → Prop
id └────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ ┴ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴ ┴ ┴
38 | intro : ∀ n x, perfect_closure.r (n, x) (n+1, frobenius α p x)
id ┴ ┴ ┴┴ ┴ ┴┴┴ └───────┘ ┴
src ┴ ┴ ┴ └───────┘
typ ┴ ┴ ┴┴ ┴ ┴┴┴ └───────┘ ┴
doc └───────┘
39 run_cmd tactic.mk_iff_of_inductive_prop `perfect_closure.r `perfect_closure.r_iff
id └─────────────────────────────┘ ┴ ┴
src └─────────────────────────────┘ ┴ ┴
typ └─────────────────────────────┘ ┴ ┴
doc └─────────────────────────────┘
40
41 /-- The perfect closure is the smallest extension that makes frobenius surjective. -/
42 def perfect_closure (α : Type u) [monoid α] (p : ℕ) : Type u :=
id └────┘ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴
43 quot (perfect_closure.r α p)
id └──┘ └───────────────┘ ┴ ┴
src └───────────────┘
typ └──┘ └───────────────┘ ┴ ┴
44
45 namespace perfect_closure
46
47 variables (α : Type u)
48
49 private lemma mul_aux_left [comm_monoid α] (p : ℕ) (x1 x2 y : ℕ × α) (H : r α p x1 x2) :
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
src └─────────┘ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
50 quot.mk (r α p) (x1.1 + y.1, ((frobenius α p)^[y.1] x1.2) * ((frobenius α p)^[x1.1] y.2)) =
id └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴
doc └───────┘ └───────┘
51 quot.mk (r α p) (x2.1 + y.1, ((frobenius α p)^[y.1] x2.2) * ((frobenius α p)^[x2.1] y.2)) :=
id └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴
doc └───────┘ └───────┘
52 match x1, x2, H with
id └┘ └┘ ┴
typ └┘ └┘ ┴
53 | _, _, r.intro _ n x := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id └─────┘ └────────┘ └──────────────┘ └───────────────┘
src └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
typ └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st └─────────────────────┘└─────────────────┘└─
54 nat.iterate_succ', ← frobenius_mul, nat.succ_add]; apply r.intro
id └───────────────┘ └───────────┘ └──────────┘ └─────┘
src ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘┴ └────┘└─────┘┴
typ ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘┴ └────┘└─────┘┴
doc ───┘ └──┘ └┘ ┴ └────┘ ┴
txt ───┘ └──┘ └┘ ┴ └────┘ ┴
par ───┘ └──┘ └┘ ┴ └────┘ ┴
pid ───┘ └──┘ └┘ ┴ ┴ ┴
st ────────────────────┘└───────────────┘└────────────┘┴└──────────────┘
55 end
56
57 private lemma mul_aux_right [comm_monoid α] (p : ℕ) (x y1 y2 : ℕ × α) (H : r α p y1 y2) :
id └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
src └─────────┘ ┴ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
58 quot.mk (r α p) (x.1 + y1.1, ((frobenius α p)^[y1.1] x.2) * ((frobenius α p)^[x.1] y1.2)) =
id └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴
doc └───────┘ └───────┘
59 quot.mk (r α p) (x.1 + y2.1, ((frobenius α p)^[y2.1] x.2) * ((frobenius α p)^[x.1] y2.2)) :=
id └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴
doc └───────┘ └───────┘
60 match y1, y2, H with
id └┘ └┘ ┴
typ └┘ └┘ ┴
61 | _, _, r.intro _ n y := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id └─────┘ └────────┘ └──────────────┘ └───────────────┘
src └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
typ └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st └─────────────────────┘└─────────────────┘└─
62 nat.iterate_succ', ← frobenius_mul]; apply r.intro
id └───────────────┘ └───────────┘ └─────┘
src ───┘└───────────────┘└──┘└───────────┘┴ └────┘└─────┘┴
typ ───┘└───────────────┘└──┘└───────────┘┴ └────┘└─────┘┴
doc ───┘ └──┘ ┴ └────┘ ┴
txt ───┘ └──┘ ┴ └────┘ ┴
par ───┘ └──┘ ┴ └────┘ ┴
pid ───┘ └──┘ ┴ ┴ ┴
st ────────────────────┘└───────────────┘┴└──────────────┘
63 end
64
65 instance [comm_monoid α] (p : ℕ) : has_mul (perfect_closure α p) :=
id └─────────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
src └─────────┘ ┴ └─────┘ └─────────────┘
typ └─────────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
66 ⟨quot.lift (λ x:ℕ×α, quot.lift (λ y:ℕ×α, quot.mk (r α p)
id └───────┘ ┴┴┴ └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴
src ┴┴ ┴┴ ┴
typ └───────┘ ┴┴┴ └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴
67 (x.1 + y.1, ((frobenius α p)^[y.1] x.2) * ((frobenius α p)^[x.1] y.2))) (mul_aux_right α p x))
id ┴┴┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ └───────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ └───────────┘
typ ┴┴┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ └───────────┘ ┴ ┴ ┴
doc └───────┘ └───────┘
68 (λ x1 x2 (H : r α p x1 x2), funext $ λ e, quot.induction_on e $ λ y,
id └┘ └┘ ┴ ┴ ┴ └┘ └┘ └────┘ ┴ └───────────────┘ ┴ ┴
src ┴ └────┘ └───────────────┘
typ └┘ └┘ ┴ ┴ ┴ └┘ └┘ └────┘ ┴ └───────────────┘ ┴ ┴
69 mul_aux_left α p x1 x2 y H)⟩
id └──────────┘ ┴ ┴ └┘ └┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ └┘ └┘ ┴ ┴
70
71 instance [comm_monoid α] (p : ℕ) : comm_monoid (perfect_closure α p) :=
id └─────────┘ ┴ ┴ └─────────┘ └─────────────┘ ┴ ┴
src └─────────┘ ┴ └─────────┘ └─────────────┘
typ └─────────┘ ┴ ┴ └─────────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
72 { mul_assoc := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
73 quot.induction_on g $ λ ⟨s, z⟩, congr_arg (quot.mk _) $
id └───────────────┘ ┴ ┴ └───────┘ └─────┘
src └───────────────┘ └───────┘
typ └───────────────┘ ┴ ┴ └───────┘ └─────┘
74 by simp only [add_assoc, mul_assoc, nat.iterate₂ (frobenius_mul _ _),
id └───────┘ └───────┘ └──────────┘ └───────────┘
src └─────────┘└───────┘└┘└───────┘└┘└──────────┘┴ └───────────┘└──────
typ └─────────┘└───────┘└┘└───────┘└┘└──────────┘┴ └───────────┘└──────
doc └─────────┘ └┘ └┘ ┴ └──────
txt └─────────┘ └┘ └┘ ┴ └──────
par └─────────┘ └┘ └┘ ┴ └──────
pid ┴└──┘└┘ └┘ └┘ ┴ └──────
st └───────────────────────────────────────────────────────────────────
75 (nat.iterate_add _ _ _ _).symm, add_comm, add_left_comm],
id └─────────────┘ └──────┘ └───────────┘
src ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘┴
typ ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘┴
doc ─────┘ └──────────────┘ └┘ ┴
txt ─────┘ └──────────────┘ └┘ ┴
par ─────┘ └──────────────┘ └┘ ┴
pid ─────┘ └──────────────┘ └┘ ┴
st ─────────────────────────────────────────────────────────────┘
76 one := quot.mk _ (0, 1),
id └─────┘ ┴
src ┴
typ └─────┘ ┴
77 one_mul := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
src └───────────────┘ └───────┘
typ ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
78 by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate_zero, one_mul, zero_add]),
id └──────────┘ └───────────┘ └──────────────┘ └─────┘ └──────┘
src └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘┴
typ └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘┴
doc └─────────┘ ┴ └─────┘ └┘ └┘ ┴
txt └─────────┘ ┴ └─────┘ └┘ └┘ ┴
par └─────────┘ ┴ └─────┘ └┘ └┘ ┴
pid ┴└──┘└┘ ┴ └─────┘ └┘ └┘ ┴
st └────────────────────────────────────────────────────────────────────────────────┘
79 mul_one := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
src └───────────────┘ └───────┘
typ ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
80 by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate_zero, mul_one, add_zero]),
id └──────────┘ └───────────┘ └──────────────┘ └─────┘ └──────┘
src └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘┴
typ └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────────┘└┘└─────┘└┘└──────┘┴
doc └─────────┘ ┴ └─────┘ └┘ └┘ ┴
txt └─────────┘ ┴ └─────┘ └┘ └┘ ┴
par └─────────┘ ┴ └─────┘ └┘ └┘ ┴
pid ┴└──┘└┘ ┴ └─────┘ └┘ └┘ ┴
st └────────────────────────────────────────────────────────────────────────────────┘
81 mul_comm := λ e f, quot.induction_on e (λ ⟨m, x⟩, quot.induction_on f (λ ⟨n, y⟩,
id ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
82 congr_arg (quot.mk _) $ by simp only [add_comm, mul_comm])),
id └───────┘ └─────┘ └──────┘ └──────┘
src └───────┘ └─────────┘└──────┘└┘└──────┘┴
typ └───────┘ └─────┘ └─────────┘└──────┘└┘└──────┘┴
doc └─────────┘ └┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └─────────────────────────────┘
83 .. (infer_instance : has_mul (perfect_closure α p)) }
id └────────────┘ └─────┘ └─────────────┘ ┴ ┴
src └────────────┘ └─────┘ └─────────────┘
typ └────────────┘ └─────┘ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
84
85 instance [comm_monoid α] (p) : inhabited (perfect_closure α p) := ⟨1⟩
id └─────────┘ ┴ └───────┘ └─────────────┘ ┴ ┴
src └─────────┘ └───────┘ └─────────────┘
typ └─────────┘ ┴ └───────┘ └─────────────┘ ┴ ┴
doc └─────────────┘
86
87 private lemma add_aux_left [comm_ring α] (p : ℕ) (hp : nat.prime p) [char_p α p]
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
doc └───────┘ └────┘
88 (x1 x2 y : ℕ × α) (H : r α p x1 x2) :
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
89 quot.mk (r α p) (x1.1 + y.1, ((frobenius α p)^[y.1] x1.2) + ((frobenius α p)^[x1.1] y.2)) =
id └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴
doc └───────┘ └───────┘
90 quot.mk (r α p) (x2.1 + y.1, ((frobenius α p)^[y.1] x2.2) + ((frobenius α p)^[x2.1] y.2)) :=
id └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴└┘┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴
doc └───────┘ └───────┘
91 match x1, x2, H with
id └┘ └┘ ┴
typ └┘ └┘ ┴
92 | _, _, r.intro _ n x := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id └─────┘ └────────┘ └──────────────┘ └───────────────┘
src └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
typ └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st └─────────────────────┘└─────────────────┘└─
93 nat.iterate_succ', ← frobenius_add, nat.succ_add]; apply r.intro
id └───────────────┘ └───────────┘ └──────────┘ └─────┘
src ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘┴ └────┘└─────┘┴
typ ───┘└───────────────┘└──┘└───────────┘└┘└──────────┘┴ └────┘└─────┘┴
doc ───┘ └──┘ └┘ ┴ └────┘ ┴
txt ───┘ └──┘ └┘ ┴ └────┘ ┴
par ───┘ └──┘ └┘ ┴ └────┘ ┴
pid ───┘ └──┘ └┘ ┴ ┴ ┴
st ────────────────────┘└───────────────┘└────────────┘┴└──────────────┘
94 end
95
96 private lemma add_aux_right [comm_ring α] (p : ℕ) (hp : nat.prime p) [char_p α p]
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
doc └───────┘ └────┘
97 (x y1 y2 : ℕ × α) (H : r α p y1 y2) :
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘
98 quot.mk (r α p) (x.1 + y1.1, ((frobenius α p)^[y1.1] x.2) + ((frobenius α p)^[x.1] y1.2)) =
id └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴ ┴
doc └───────┘ └───────┘
99 quot.mk (r α p) (x.1 + y2.1, ((frobenius α p)^[y2.1] x.2) + ((frobenius α p)^[x.1] y2.2)) :=
id └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴
src ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ └┘┴ └───────┘ ┴ ┴ └┘└┘┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ └┘┴
doc └───────┘ └───────┘
100 match y1, y2, H with
id └┘ └┘ ┴
typ └┘ └┘ ┴
101 | _, _, r.intro _ n y := quot.sound $ by rw [← nat.iterate_succ, nat.iterate_succ',
id └─────┘ └────────┘ └──────────────┘ └───────────────┘
src └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
typ └─────┘ └────────┘ └────┘└──────────────┘└┘└───────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st └─────────────────────┘└─────────────────┘└─
102 nat.iterate_succ', ← frobenius_add]; apply r.intro
id └───────────────┘ └───────────┘ └─────┘
src ───┘└───────────────┘└──┘└───────────┘┴ └────┘└─────┘┴
typ ───┘└───────────────┘└──┘└───────────┘┴ └────┘└─────┘┴
doc ───┘ └──┘ ┴ └────┘ ┴
txt ───┘ └──┘ ┴ └────┘ ┴
par ───┘ └──┘ ┴ └────┘ ┴
pid ───┘ └──┘ ┴ ┴ ┴
st ────────────────────┘└───────────────┘┴└──────────────┘
103 end
104
105 instance [comm_ring α] (p : ℕ) [hp : nat.prime p] [char_p α p] : has_add (perfect_closure α p) :=
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ └─────┘ └─────────────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
doc └───────┘ └────┘ └─────────────┘
106 ⟨quot.lift (λ x:ℕ×α, quot.lift (λ y:ℕ×α, quot.mk (r α p)
id └───────┘ ┴┴┴ └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴
src ┴┴ ┴┴ ┴
typ └───────┘ ┴┴┴ └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴
107 (x.1 + y.1, ((frobenius α p)^[y.1] x.2) + ((frobenius α p)^[x.1] y.2))) (add_aux_right α p hp x))
id ┴┴┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ └───────────┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ └───────────┘
typ ┴┴┴ ┴ ┴┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴ └┘┴┴ ┴ ┴┴ └───────────┘ ┴ ┴ └┘ ┴
doc └───────┘ └───────┘
108 (λ x1 x2 (H : r α p x1 x2), funext $ λ e, quot.induction_on e $ λ y,
id └┘ └┘ ┴ ┴ ┴ └┘ └┘ └────┘ ┴ └───────────────┘ ┴ ┴
src ┴ └────┘ └───────────────┘
typ └┘ └┘ ┴ ┴ ┴ └┘ └┘ └────┘ ┴ └───────────────┘ ┴ ┴
109 add_aux_left α p hp x1 x2 y H)⟩
id └──────────┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴
src └──────────┘
typ └──────────┘ ┴ ┴ └┘ └┘ └┘ ┴ ┴
110
111 instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : has_neg (perfect_closure α p) :=
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ └─────┘ └─────────────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
doc └───────┘ └────┘ └─────────────┘
112 ⟨quot.lift (λ x:ℕ×α, quot.mk (r α p) (x.1, -x.2)) (λ x y (H : r α p x y), match x, y, H with
id └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
113 | _, _, r.intro _ n x := quot.sound $ by rw ← frobenius_neg; apply r.intro
id └─────┘ └────────┘ └───────────┘ └─────┘
src └─────┘ └────────┘ └───┘└───────────┘ └────┘└─────┘┴
typ └─────┘ └────────┘ └───┘└───────────┘ └────┘└─────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid └─┘ ┴ ┴
st └─────────────────────────────────┘
114 end)⟩
115
116 theorem mk_zero [comm_ring α] (p : ℕ) [nat.prime p] (n : ℕ) : quot.mk (r α p) (n, 0) = quot.mk (r α p) (0, 0) :=
id └───────┘ ┴ ┴ └───────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ └───────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └───────┘
117 by induction n with n ih; [refl, rw ← ih]; symmetry; apply quot.sound;
id ┴ ┴ └┘ └────────┘
src └────────┘ └────────┘ ┴└──┘ └───┘ └──────┘ └────┘└────────┘
typ └────────┘┴└────────┘ ┴└──┘ └───┘└┘ └──────┘ └────┘└────────┘
doc └────────┘ └────────┘ └──┘ └───┘ └──────┘ └────┘
txt └────────┘ └────────┘ └──┘ └───┘ └──────┘ └────┘
par └────────┘ └────────┘ └──┘ └───┘ └──────┘ └────┘
pid ┴ ┴└───────┘ └─┘ ┴
st └────────────────────────────────────────────────────────────────────
118 have := r.intro p n (0:α); rwa [frobenius_zero α p] at this
id └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └──────┘└─────┘┴ ┴ ┴ └┘ ┴ └───┘└────────────┘┴ ┴ └─────────
typ └──────┘└─────┘┴┴┴┴┴ └┘┴┴ └───┘└────────────┘┴┴┴┴└─────────
doc └──────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └─────────
txt └──────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └─────────
par └──────┘ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ └─────────
pid └───┘└─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴└──────┘└
st ───────────────────────────────┘└────────────────┘┴└────────
119
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
120 theorem r.sound [monoid α] (p m n : ℕ) (x y : α) (H : frobenius α p^[m] x = y) :
id └────┘ ┴ ┴ ┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴ ┴
src └────┘ ┴ └───────┘ └┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴ ┴
doc └───────┘
121 quot.mk (r α p) (n, x) = quot.mk (r α p) (m + n, y) :=
id └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
122 by subst H; induction m with m ih; [simp only [zero_add, nat.iterate_zero],
id ┴ ┴ ┴ └──────┘ └──────────────┘
src └────┘ └────────┘ └────────┘ ┴└─────────┘└──────┘└┘└──────────────┘┴
typ └────┘┴ └────────┘┴└────────┘ ┴└─────────┘└──────┘└┘└──────────────┘┴
doc └────┘ └────────┘ └────────┘ └─────────┘ └┘ ┴
txt └────┘ └────────┘ └────────┘ └─────────┘ └┘ ┴
par └────┘ └────────┘ └────────┘ └─────────┘ └┘ ┴
pid ┴ ┴ ┴└───────┘ ┴└──┘└┘ └┘ ┴
st └─────────────────────────────────────────────────────────────────────────
123 rw [ih, nat.succ_add, nat.iterate_succ']]; apply quot.sound; apply r.intro
id └┘ └──────────┘ └───────────────┘ └────────┘ └─────┘
src └──┘ └┘└──────────┘└┘└───────────────┘┴ └────┘└────────┘ └────┘└─────┘└
typ └──┘└┘└┘└──────────┘└┘└───────────────┘┴ └────┘└────────┘ └────┘└─────┘└
doc └──┘ └┘ └┘ ┴ └────┘ └────┘ └
txt └──┘ └┘ └┘ ┴ └────┘ └────┘ └
par └──┘ └┘ └┘ ┴ └────┘ └────┘ └
pid └┘ └┘ └┘ ┴ ┴ ┴ └
st ─────┘└┘└────────────┘└─────────────────┘┴└──────────────────────────────────
124
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
125 instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : comm_ring (perfect_closure α p) :=
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────┘ └─────────────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ └───────┘ └─────────────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────┘ └─────────────┘ ┴ ┴
doc └───────┘ └────┘ └─────────────┘
126 { add_assoc := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
127 quot.induction_on g $ λ ⟨s, z⟩, congr_arg (quot.mk _) $
id └───────────────┘ ┴ ┴ └───────┘ └─────┘
src └───────────────┘ └───────┘
typ └───────────────┘ ┴ ┴ └───────┘ └─────┘
128 by simp only [add_assoc, nat.iterate₂ (frobenius_add α p),
id └───────┘ └──────────┘ └───────────┘ ┴ ┴
src └─────────┘└───────┘└┘└──────────┘┴ └───────────┘┴ ┴ └──
typ └─────────┘└───────┘└┘└──────────┘┴ └───────────┘┴┴┴┴└──
doc └─────────┘ └┘ ┴ ┴ ┴ └──
txt └─────────┘ └┘ ┴ ┴ ┴ └──
par └─────────┘ └┘ ┴ ┴ ┴ └──
pid ┴└──┘└┘ └┘ ┴ ┴ ┴ └──
st └────────────────────────────────────────────────────────
129 (nat.iterate_add _ _ _ _).symm, add_comm, add_left_comm],
id └─────────────┘ └──────┘ └───────────┘
src ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘┴
typ ─────┘ └─────────────┘└──────────────┘└──────┘└┘└───────────┘┴
doc ─────┘ └──────────────┘ └┘ ┴
txt ─────┘ └──────────────┘ └┘ ┴
par ─────┘ └──────────────┘ └┘ ┴
pid ─────┘ └──────────────┘ └┘ ┴
st ─────────────────────────────────────────────────────────────┘
130 zero := quot.mk _ (0, 0),
id └─────┘ ┴
src ┴
typ └─────┘ ┴
131 zero_add := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
src └───────────────┘ └───────┘
typ ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
132 by simp only [nat.iterate₀ (frobenius_zero α p), nat.iterate_zero, zero_add]),
id └──────────┘ └────────────┘ ┴ ┴ └──────────────┘ └──────┘
src └─────────┘└──────────┘┴ └────────────┘┴ ┴ └─┘└──────────────┘└┘└──────┘┴
typ └─────────┘└──────────┘┴ └────────────┘┴┴┴┴└─┘└──────────────┘└┘└──────┘┴
doc └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴
txt └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴
par └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴ └─┘ └┘ ┴
st └────────────────────────────────────────────────────────────────────────┘
133 add_zero := λ e, quot.induction_on e (λ ⟨n, x⟩, congr_arg (quot.mk _) $
id ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
src └───────────────┘ └───────┘
typ ┴ └───────────────┘ ┴ ┴ └───────┘ └─────┘
134 by simp only [nat.iterate₀ (frobenius_zero α p), nat.iterate_zero, add_zero]),
id └──────────┘ └────────────┘ ┴ ┴ └──────────────┘ └──────┘
src └─────────┘└──────────┘┴ └────────────┘┴ ┴ └─┘└──────────────┘└┘└──────┘┴
typ └─────────┘└──────────┘┴ └────────────┘┴┴┴┴└─┘└──────────────┘└┘└──────┘┴
doc └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴
txt └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴
par └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴
pid ┴└──┘└┘ ┴ ┴ ┴ └─┘ └┘ ┴
st └────────────────────────────────────────────────────────────────────────┘
135 add_left_neg := λ e, quot.induction_on e (λ ⟨n, x⟩, show quot.mk _ _ = _,
id ┴ └───────────────┘ ┴ ┴ └─────┘ ┴
src └───────────────┘ ┴
typ ┴ └───────────────┘ ┴ ┴ └─────┘ ┴
136 by simp only [nat.iterate₁ (frobenius_neg α p), add_left_neg, mk_zero]; refl),
id └──────────┘ └───────────┘ ┴ ┴ └──────────┘ └─────┘
src └─────────┘└──────────┘┴ └───────────┘┴ ┴ └─┘└──────────┘└┘└─────┘┴ └──┘
typ └─────────┘└──────────┘┴ └───────────┘┴┴┴┴└─┘└──────────┘└┘└─────┘┴ └──┘
doc └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ └──┘
txt └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ └──┘
par └─────────┘ ┴ ┴ ┴ └─┘ └┘ ┴ └──┘
pid ┴└──┘└┘ ┴ ┴ ┴ └─┘ └┘ ┴
st └────────────────────────────────────────────────────────────────────────┘
137 add_comm := λ e f, quot.induction_on e (λ ⟨m, x⟩, quot.induction_on f (λ ⟨n, y⟩,
id ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
138 congr_arg (quot.mk _) $ by simp only [add_comm])),
id └───────┘ └─────┘ └──────┘
src └───────┘ └─────────┘└──────┘┴
typ └───────┘ └─────┘ └─────────┘└──────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st └───────────────────┘
139 left_distrib := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
140 quot.induction_on g $ λ ⟨s, z⟩, show quot.mk _ _ = quot.mk _ _,
id └───────────────┘ ┴ ┴ └─────┘ ┴ └─────┘
src └───────────────┘ ┴
typ └───────────────┘ ┴ ┴ └─────┘ ┴ └─────┘
141 by simp only [add_assoc, add_comm, add_left_comm]; apply r.sound;
id └───────┘ └──────┘ └───────────┘ └─────┘
src └─────────┘└───────┘└┘└──────┘└┘└───────────┘┴ └────┘└─────┘
typ └─────────┘└───────┘└┘└──────┘└┘└───────────┘┴ └────┘└─────┘
doc └─────────┘ └┘ └┘ ┴ └────┘
txt └─────────┘ └┘ └┘ ┴ └────┘
par └─────────┘ └┘ └┘ ┴ └────┘
pid ┴└──┘└┘ └┘ └┘ ┴ ┴
st └───────────────────────────────────────────────────────────────
142 simp only [nat.iterate₂ (frobenius_mul α p), nat.iterate₂ (frobenius_add α p),
id └──────────┘ └───────────┘ ┴ ┴ └──────────┘ └───────────┘ ┴ ┴
src └─────────┘└──────────┘┴ └───────────┘┴ ┴ └─┘└──────────┘┴ └───────────┘┴ ┴ └──
typ └─────────┘└──────────┘┴ └───────────┘┴┴┴┴└─┘└──────────┘┴ └───────────┘┴┴┴┴└──
doc └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
txt └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
par └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
pid ┴└──┘└┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────────────────────
143 (nat.iterate_add _ _ _ _).symm, mul_add, add_comm, add_left_comm],
id └─────────────┘ └─────┘ └──────┘ └───────────┘
src ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘┴
typ ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘┴
doc ─────┘ └──────────────┘ └┘ └┘ ┴
txt ─────┘ └──────────────┘ └┘ └┘ ┴
par ─────┘ └──────────────┘ └┘ └┘ ┴
pid ─────┘ └──────────────┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────┘
144 right_distrib := λ e f g, quot.induction_on e $ λ ⟨m, x⟩, quot.induction_on f $ λ ⟨n, y⟩,
id ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
145 quot.induction_on g $ λ ⟨s, z⟩, show quot.mk _ _ = quot.mk _ _,
id └───────────────┘ ┴ ┴ └─────┘ ┴ └─────┘
src └───────────────┘ ┴
typ └───────────────┘ ┴ ┴ └─────┘ ┴ └─────┘
146 by simp only [add_assoc, add_comm _ s, add_left_comm _ s]; apply r.sound;
id └───────┘ └──────┘ ┴ └───────────┘ ┴ └─────┘
src └─────────┘└───────┘└┘└──────┘└─┘ └┘└───────────┘└─┘ ┴ └────┘└─────┘
typ └─────────┘└───────┘└┘└──────┘└─┘┴└┘└───────────┘└─┘┴┴ └────┘└─────┘
doc └─────────┘ └┘ └─┘ └┘ └─┘ ┴ └────┘
txt └─────────┘ └┘ └─┘ └┘ └─┘ ┴ └────┘
par └─────────┘ └┘ └─┘ └┘ └─┘ ┴ └────┘
pid ┴└──┘└┘ └┘ └─┘ └┘ └─┘ ┴ ┴
st └───────────────────────────────────────────────────────────────────────
147 simp only [nat.iterate₂ (frobenius_mul α p), nat.iterate₂ (frobenius_add α p),
id └──────────┘ └───────────┘ ┴ ┴ └──────────┘ └───────────┘ ┴ ┴
src └─────────┘└──────────┘┴ └───────────┘┴ ┴ └─┘└──────────┘┴ └───────────┘┴ ┴ └──
typ └─────────┘└──────────┘┴ └───────────┘┴┴┴┴└─┘└──────────┘┴ └───────────┘┴┴┴┴└──
doc └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
txt └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
par └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
pid ┴└──┘└┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └──
st ───────────────────────────────────────────────────────────────────────────────────
148 (nat.iterate_add _ _ _ _).symm, add_mul, add_comm, add_left_comm],
id └─────────────┘ └─────┘ └──────┘ └───────────┘
src ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘┴
typ ─────┘ └─────────────┘└──────────────┘└─────┘└┘└──────┘└┘└───────────┘┴
doc ─────┘ └──────────────┘ └┘ └┘ ┴
txt ─────┘ └──────────────┘ └┘ └┘ ┴
par ─────┘ └──────────────┘ └┘ └┘ ┴
pid ─────┘ └──────────────┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────────────────────────┘
149 .. (infer_instance : has_add (perfect_closure α p)),
id └────────────┘ └─────┘ └─────────────┘ ┴ ┴
src └────────────┘ └─────┘ └─────────────┘
typ └────────────┘ └─────┘ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
150 .. (infer_instance : has_neg (perfect_closure α p)),
id └────────────┘ └─────┘ └─────────────┘ ┴ ┴
src └────────────┘ └─────┘ └─────────────┘
typ └────────────┘ └─────┘ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
151 .. (infer_instance : comm_monoid (perfect_closure α p)) }
id └────────────┘ └─────────┘ └─────────────┘ ┴ ┴
src └────────────┘ └─────────┘ └─────────────┘
typ └────────────┘ └─────────┘ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
152
153 instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : has_inv (perfect_closure α p) :=
id └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
src └────────────┘ ┴ └───────┘ └────┘ └─────┘ └─────────────┘
typ └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────┘ └─────────────┘ ┴ ┴
doc └───────┘ └────┘ └─────────────┘
154 ⟨quot.lift (λ x:ℕ×α, quot.mk (r α p) (x.1, x.2⁻¹)) (λ x y (H : r α p x y), match x, y, H with
id └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴┴ ┴ ┴ ┴ ┴ └┘ ┴
typ └───────┘ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
155 | _, _, r.intro _ n x := quot.sound $ by simp only [frobenius]; rw ← inv_pow'; apply r.intro
id └─────┘ └────────┘ └───────┘ └──────┘ └─────┘
src └─────┘ └────────┘ └─────────┘└───────┘┴ └───┘└──────┘ └────┘└─────┘┴
typ └─────┘ └────────┘ └─────────┘└───────┘┴ └───┘└──────┘ └────┘└─────┘┴
doc └─────────┘└───────┘┴ └───┘ └────┘ ┴
txt └─────────┘ ┴ └───┘ └────┘ ┴
par └─────────┘ ┴ └───┘ └────┘ ┴
pid ┴└──┘└┘ ┴ └─┘ ┴ ┴
st └───────────────────────────────────────────────────┘
156 end)⟩
157
158 theorem eq_iff' [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p]
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
doc └───────┘ └────┘
159 (x y : ℕ × α) : quot.mk (r α p) x = quot.mk (r α p) y ↔
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
160 ∃ z, (frobenius α p^[y.1 + z] x.2) = (frobenius α p^[x.1 + z] y.2) :=
id ┴ ┴┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴ ┴┴ ┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴ ┴┴
src ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴ ┴┴ ┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴ ┴┴
doc └───────┘ └───────┘
161 begin
st └─────
162 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
163 { intro H,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ───┘└─────┘└─
164 replace H := quot.exact _ H,
id └────────┘ ┴
src └───────────┘└────────┘└─┘
typ └───────────┘└────────┘└─┘┴
doc └───────────┘ └─┘
txt └───────────┘ └─┘
par └───────────┘ └─┘
pid └┘┴└─┘ └─┘
st ──────────────────────────────┘└─
165 induction H,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ──────────────┘└─
166 case eqv_gen.rel : x y H
src └────────────────────────
typ └────────────────────────
doc └────────────────────────
txt └────────────────────────
par └────────────────────────
pid └──────────┘└──────┘└
st ─────────────────────────────
167 { cases H with n x, exact ⟨0, rfl⟩ },
id ┴ └─┘
src ─────┘└────┘ └───────┘└┘└────┘ └─┘└─┘└┘┴
typ ─────┘└────┘┴└───────┘└┘└────┘ └─┘└─┘└┘┴
doc ─────┘└────┘ └───────┘└┘└────┘ └─┘ └┘┴
txt ─────┘└────┘ └───────┘└┘└────┘ └─┘ └┘┴
par ─────┘└────┘ └───────┘└┘└────┘ └─┘ └┘┴
pid ───────────┘ └───────────────┘ └─┘ └─┘
st ────┘└───────────────┘└───────────────┘└┘└
168 case eqv_gen.refl : H
src └─────────────────────
typ └─────────────────────
doc └─────────────────────
txt └─────────────────────
par └─────────────────────
pid └───────────┘└──┘└
st ──────────────────────────
169 { exact ⟨0, rfl⟩ },
id └─┘
src ─────┘└────┘ └─┘└─┘└┘┴
typ ─────┘└────┘ └─┘└─┘└┘┴
doc ─────┘└────┘ └─┘ └┘┴
txt ─────┘└────┘ └─┘ └┘┴
par ─────┘└────┘ └─┘ └┘┴
pid ───────────┘ └─┘ └─┘
st ────┘└──────────────┘└┘└
170 case eqv_gen.symm : x y H ih
src └────────────────────────────
typ └────────────────────────────
doc └────────────────────────────
txt └────────────────────────────
par └────────────────────────────
pid └───────────┘└─────────┘└
st ─────────────────────────────────
171 { cases ih with w ih, exact ⟨w, ih.symm⟩ },
id └┘ ┴ └─────┘
src ─────┘└────┘ └────────┘└┘└────┘ └┘└─────┘└┘┴
typ ─────┘└────┘└┘└────────┘└┘└────┘ ┴└┘└─────┘└┘┴
doc ─────┘└────┘ └────────┘└┘└────┘ └┘ └┘┴
txt ─────┘└────┘ └────────┘└┘└────┘ └┘ └┘┴
par ─────┘└────┘ └────────┘└┘└────┘ └┘ └┘┴
pid ───────────┘ └────────────────┘ └┘ └─┘
st ────┘└─────────────────┘└───────────────────┘└┘└
172 case eqv_gen.trans : x y z H1 H2 ih1 ih2
src └────────────────────────────────────────
typ └────────────────────────────────────────
doc └────────────────────────────────────────
txt └────────────────────────────────────────
par └────────────────────────────────────────
pid └────────────┘└────────────────────┘└
st ─────────────────────────────────────────────
173 { cases ih1 with z1 ih1,
id └─┘
src ─────┘└────┘ └──────────┘└─
typ ─────┘└────┘└─┘└──────────┘└─
doc ─────┘└────┘ └──────────┘└─
txt ─────┘└────┘ └──────────┘└─
par ─────┘└────┘ └──────────┘└─
pid ───────────┘ └─────────────
st ────┘└────────────────────┘└─
174 cases ih2 with z2 ih2,
id └─┘
src ─────┘└────┘ └──────────┘└─
typ ─────┘└────┘└─┘└──────────┘└─
doc ─────┘└────┘ └──────────┘└─
txt ─────┘└────┘ └──────────┘└─
par ─────┘└────┘ └──────────┘└─
pid ───────────┘ └─────────────
st ──────────────────────────┘└─
175 existsi z2+(y.1+z1),
id └┘┴ ┴ └┘
src ─────┘└──────┘ ┴ └┘ ┴└─
typ ─────┘└──────┘└┘┴ ┴└┘ └┘┴└─
doc ─────┘└──────┘ └┘ ┴└─
txt ─────┘└──────┘ └┘ ┴└─
par ─────┘└──────┘ └┘ ┴└─
pid ─────────────┘ └┘ └──
st ────────────────────────┘└─
176 rw [← add_assoc, nat.iterate_add, ih1],
id └───────┘ └─────────────┘ └─┘
src ─────┘└────┘└───────┘└┘└─────────────┘└┘ ┴└─
typ ─────┘└────┘└───────┘└┘└─────────────┘└┘└─┘┴└─
doc ─────┘└────┘ └┘ └┘ ┴└─
txt ─────┘└────┘ └┘ └┘ ┴└─
par ─────┘└────┘ └┘ └┘ ┴└─
pid ───────────┘ └┘ └┘ └──
st ────────────────────┘└───────────────┘└───┘└──
177 rw [← nat.iterate_add, add_comm, nat.iterate_add, ih2],
id └─────────────┘ └──────┘ └─────────────┘ └─┘
src ─────┘└────┘└─────────────┘└┘└──────┘└┘└─────────────┘└┘ ┴└─
typ ─────┘└────┘└─────────────┘└┘└──────┘└┘└─────────────┘└┘└─┘┴└─
doc ─────┘└────┘ └┘ └┘ └┘ ┴└─
txt ─────┘└────┘ └┘ └┘ └┘ ┴└─
par ─────┘└────┘ └┘ └┘ └┘ ┴└─
pid ───────────┘ └┘ └┘ └┘ └──
st ──────────────────────────┘└────────┘└───────────────┘└───┘└──
178 rw [← nat.iterate_add],
id └─────────────┘
src ─────┘└────┘└─────────────┘┴└─
typ ─────┘└────┘└─────────────┘┴└─
doc ─────┘└────┘ ┴└─
txt ─────┘└────┘ ┴└─
par ─────┘└────┘ ┴└─
pid ───────────┘ └──
st ──────────────────────────┘└──
179 simp only [add_comm, add_left_comm] } },
id └──────┘ └───────────┘
src ─────┘└─────────┘└──────┘└┘└───────────┘└┘└┘
typ ─────┘└─────────┘└──────┘└┘└───────────┘└┘└┘
doc ─────┘└─────────┘ └┘ └┘└┘
txt ─────┘└─────────┘ └┘ └┘└┘
par ─────┘└─────────┘ └┘ └┘└┘
pid ────────────────┘ └┘ └─┘┴
st ─────────────────────────────────────────┘┴┴└┘└
180 intro H,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
181 cases x with m x,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ─────────────────┘└─
182 cases y with n y,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ─────────────────┘└─
183 cases H with z H, dsimp only at H,
id ┴
src └────┘ └───────┘ └─────────────┘
typ └────┘┴└───────┘ └─────────────┘
doc └────┘ └───────┘ └─────────────┘
txt └────┘ └───────┘ └─────────────┘
par └────┘ └───────┘ └─────────────┘
pid ┴ └───────┘ └───┘┴└──┘
st ─────────────────┘└───────────────┘└─
184 rw [r.sound α p (n+z) m x _ rfl, r.sound α p (m+z) n y _ rfl, H],
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴
src └──┘└─────┘┴ ┴ ┴ └┘ ┴ └─┘└─┘└┘└─────┘┴ ┴ ┴ └┘ ┴ └─┘└─┘└┘ ┴
typ └──┘└─────┘┴┴┴┴┴ ┴ ┴└┘┴┴┴└─┘└─┘└┘└─────┘┴┴┴┴┴ ┴ ┴└┘┴┴┴└─┘└─┘└┘┴┴
doc └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴
txt └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴
par └──┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴
pid └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘ ┴
st ────────────────────────────────┘└───────────────────────────┘└─┘└──
185 rw [add_assoc, add_comm, add_comm z]
id └───────┘ └──────┘ └──────┘ ┴
src └──┘└───────┘└┘└──────┘└┘└──────┘┴ └┘
typ └──┘└───────┘└┘└──────┘└┘└──────┘┴┴└┘
doc └──┘ └┘ └┘ ┴ └┘
txt └──┘ └┘ └┘ ┴ └┘
par └──┘ └┘ └┘ ┴ └┘
pid └┘ └┘ └┘ ┴ ┴┴
st ──────────────┘└────────┘└──────────┘┴┴
186 end
st └─┘
187
188 theorem eq_iff [integral_domain α] (p : ℕ) [nat.prime p] [char_p α p]
id └─────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
src └─────────────┘ ┴ └───────┘ └────┘
typ └─────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
doc └───────┘ └────┘
189 (x y : ℕ × α) : quot.mk (r α p) x = quot.mk (r α p) y ↔
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
190 (frobenius α p^[y.1] x.2) = (frobenius α p^[x.1] y.2) :=
id └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴
src └───────┘ └┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴ ┴ └───────┘ ┴ ┴└┘┴┴ ┴ ┴┴
doc └───────┘ └───────┘
191 (eq_iff' α p x y).trans ⟨λ ⟨z, H⟩, nat.iterate_inj (frobenius_inj α p) z _ _ $
id └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴┴ └─────────────┘ └───────────┘ ┴ ┴
src └─────┘ └───┘ └─────────────┘ └───────────┘
typ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴┴ └─────────────┘ └───────────┘ ┴ ┴
192 by simpa only [add_comm, nat.iterate_add] using H,
id └──────┘ └─────────────┘ ┴
src └──────────┘└──────┘└┘└─────────────┘└──────┘
typ └──────────┘└──────┘└┘└─────────────┘└──────┘┴
doc └──────────┘ └┘ └──────┘
txt └──────────┘ └┘ └──────┘
par └──────────┘ └┘ └──────┘
pid ┴└──┘└┘ └┘ ┴┴└────┘
st └─────────────────────────────────────────────┘
193 λ H, ⟨0, H⟩⟩
id ┴ ┴
typ ┴ ┴
194
195 instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : discrete_field (perfect_closure α p) :=
id └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └────────────┘ └─────────────┘ ┴ ┴
src └────────────┘ ┴ └───────┘ └────┘ └────────────┘ └─────────────┘
typ └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └────────────┘ └─────────────┘ ┴ ┴
doc └───────┘ └────┘ └─────────────┘
196 { zero_ne_one := λ H, zero_ne_one ((eq_iff _ _ _ _).1 H),
id ┴ └─────────┘ └────┘ ┴ ┴
src └─────────┘ └────┘ ┴
typ ┴ └─────────┘ └────┘ ┴ ┴
197 mul_inv_cancel := λ e, quot.induction_on e $ λ ⟨m, x⟩ H,
id ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘
typ ┴ └───────────────┘ ┴ ┴ ┴
198 have _ := mt (eq_iff _ _ _ _).2 H, (eq_iff _ _ _ _).2
id └┘ └────┘ ┴ ┴ └────┘ ┴
src └┘ └────┘ ┴ └────┘ ┴
typ └┘ └────┘ ┴ ┴ └────┘ ┴
199 (by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate₀ (frobenius_zero α p),
id └──────────┘ └───────────┘ └──────────┘ └────────────┘ ┴ ┴
src └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────┘┴ └────────────┘┴ ┴ └──
typ └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────┘┴ └────────────┘┴┴┴┴└──
doc └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └──
txt └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └──
par └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └──
pid ┴└──┘└┘ ┴ └─────┘ ┴ ┴ ┴ └──
st └────────────────────────────────────────────────────────────────────────────────
200 nat.iterate_zero, (nat.iterate₂ (frobenius_mul α p)).symm] at this ⊢;
id └──────────────┘ └──────────┘ └───────────┘ ┴ ┴
src ───────┘└──────────────┘└┘ └──────────┘┴ └───────────┘┴ ┴ └────────────────┘
typ ───────┘└──────────────┘└┘ └──────────┘┴ └───────────┘┴┴┴┴└────────────────┘
doc ───────┘ └┘ ┴ ┴ ┴ └────────────────┘
txt ───────┘ └┘ ┴ ┴ ┴ └────────────────┘
par ───────┘ └┘ ┴ ┴ ┴ └────────────────┘
pid ───────┘ └┘ ┴ ┴ ┴ └──────┘┴└───────┘
st ──────────────────────────────────────────────────────────────────────────────
201 rw [mul_inv_cancel this, nat.iterate₀ (frobenius_one _ _)]),
id └────────────┘ └──┘ └──────────┘ └───────────┘
src └──┘└────────────┘┴ └┘└──────────┘┴ └───────────┘└────┘
typ └──┘└────────────┘┴└──┘└┘└──────────┘┴ └───────────┘└────┘
doc └──┘ ┴ └┘ ┴ └────┘
txt └──┘ ┴ └┘ ┴ └────┘
par └──┘ ┴ └┘ ┴ └────┘
pid └┘ ┴ └┘ ┴ └────┘
st ───────────┘└─────────────────┘└────────────────────────────────┘┴
202 inv_mul_cancel := λ e, quot.induction_on e $ λ ⟨m, x⟩ H,
id ┴ └───────────────┘ ┴ ┴ ┴
src └───────────────┘
typ ┴ └───────────────┘ ┴ ┴ ┴
203 have _ := mt (eq_iff _ _ _ _).2 H, (eq_iff _ _ _ _).2
id └┘ └────┘ ┴ ┴ └────┘ ┴
src └┘ └────┘ ┴ └────┘ ┴
typ └┘ └────┘ ┴ ┴ └────┘ ┴
204 (by simp only [nat.iterate₀ (frobenius_one _ _), nat.iterate₀ (frobenius_zero α p),
id └──────────┘ └───────────┘ └──────────┘ └────────────┘ ┴ ┴
src └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────┘┴ └────────────┘┴ ┴ └──
typ └─────────┘└──────────┘┴ └───────────┘└─────┘└──────────┘┴ └────────────┘┴┴┴┴└──
doc └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └──
txt └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └──
par └─────────┘ ┴ └─────┘ ┴ ┴ ┴ └──
pid ┴└──┘└┘ ┴ └─────┘ ┴ ┴ ┴ └──
st └────────────────────────────────────────────────────────────────────────────────
205 nat.iterate_zero, (nat.iterate₂ (frobenius_mul α p)).symm] at this ⊢;
id └──────────────┘ └──────────┘ └───────────┘ ┴ ┴
src ───────┘└──────────────┘└┘ └──────────┘┴ └───────────┘┴ ┴ └────────────────┘
typ ───────┘└──────────────┘└┘ └──────────┘┴ └───────────┘┴┴┴┴└────────────────┘
doc ───────┘ └┘ ┴ ┴ ┴ └────────────────┘
txt ───────┘ └┘ ┴ ┴ ┴ └────────────────┘
par ───────┘ └┘ ┴ ┴ ┴ └────────────────┘
pid ───────┘ └┘ ┴ ┴ ┴ └──────┘┴└───────┘
st ──────────────────────────────────────────────────────────────────────────────
206 rw [inv_mul_cancel this, nat.iterate₀ (frobenius_one _ _)]),
id └────────────┘ └──┘ └──────────┘ └───────────┘
src └──┘└────────────┘┴ └┘└──────────┘┴ └───────────┘└────┘
typ └──┘└────────────┘┴└──┘└┘└──────────┘┴ └───────────┘└────┘
doc └──┘ ┴ └┘ ┴ └────┘
txt └──┘ ┴ └┘ ┴ └────┘
par └──┘ ┴ └┘ ┴ └────┘
pid └┘ ┴ └┘ ┴ └────┘
st ───────────┘└─────────────────┘└────────────────────────────────┘┴
207 has_decidable_eq := λ e f, quot.rec_on_subsingleton e $ λ ⟨m, x⟩,
id ┴ ┴ └──────────────────────┘ ┴ ┴
src └──────────────────────┘
typ ┴ ┴ └──────────────────────┘ ┴ ┴
208 quot.rec_on_subsingleton f $ λ ⟨n, y⟩,
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴ ┴
209 decidable_of_iff' _ (eq_iff α p _ _),
id └───────────────┘ └────┘ ┴ ┴
src └───────────────┘ └────┘
typ └───────────────┘ └────┘ ┴ ┴
210 inv_zero := congr_arg (quot.mk (r α p)) (by rw [inv_zero]),
id └───────┘ └─────┘ ┴ ┴ ┴ └──────┘
src └───────┘ ┴ └──┘└──────┘┴
typ └───────┘ └─────┘ ┴ ┴ ┴ └──┘└──────┘┴
doc └──┘ ┴
txt └──┘ ┴
par └──┘ ┴
pid └┘ ┴
st └───────────┘┴
211 .. (infer_instance : has_inv (perfect_closure α p)),
id └────────────┘ └─────┘ └─────────────┘ ┴ ┴
src └────────────┘ └─────┘ └─────────────┘
typ └────────────┘ └─────┘ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
212 .. (infer_instance : comm_ring (perfect_closure α p)) }
id └────────────┘ └───────┘ └─────────────┘ ┴ ┴
src └────────────┘ └───────┘ └─────────────┘
typ └────────────┘ └───────┘ └─────────────┘ ┴ ┴
doc └────────────┘ └─────────────┘
213
214 theorem frobenius_mk [comm_monoid α] (p : ℕ) (x : ℕ × α) :
id └─────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ ┴ ┴
215 frobenius (perfect_closure α p) p (quot.mk (r α p) x) = quot.mk _ (x.1, x.2^p) :=
id └───────┘ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴┴ ┴┴ ┴┴
src └───────┘ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴┴┴ ┴┴ ┴┴
doc └───────┘ └─────────────┘
216 begin
st └─────
217 unfold frobenius, cases x with n x, dsimp only,
id ┴
src └──────────────┘ └────┘ └───────┘ └────────┘
typ └──────────────┘ └────┘┴└───────┘ └────────┘
doc └──────────────┘ └────┘ └───────┘ └────────┘
txt └──────────────┘ └────┘ └───────┘ └────────┘
par └──────────────┘ └────┘ └───────┘ └────────┘
pid └────────┘ ┴ └───────┘ └───┘
st ─────────────────┘└────────────────┘└──────────┘└─
218 suffices : ∀ p':ℕ, (quot.mk (r α p) (n, x) ^ p' : perfect_closure α p) = quot.mk (r α p) (n, x ^ p'),
id ┴ └─────────────┘ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴
src └─────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘┴┴ └─┘└─────────────┘┴ ┴ └┘┴┴ ┴ ┴┴ ┴ └┘┴ └┘ ┴ ┴ ┴
typ └─────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘┴┴ └─┘└─────────────┘┴ ┴ └┘┴┴└─────┘┴ ┴┴┴┴┴└┘┴┴└┘┴┴ ┴ ┴
doc └─────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └─┘└─────────────┘┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
txt └─────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
par └─────────┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
pid └───────┘└┘ └──┘ ┴ ┴ ┴ ┴ └┘ └┘ └┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
219 { apply this },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└─────────┘└┘└
220 intro p, induction p with p ih,
id ┴
src └─────┘ └────────┘ └────────┘
typ └─────┘ └────────┘┴└────────┘
doc └─────┘ └────────┘ └────────┘
txt └─────┘ └────────┘ └────────┘
par └─────┘ └────────┘ └────────┘
pid └┘ ┴ ┴└───────┘
st ────────┘└─────────────────────┘└─
221 case nat.zero { apply r.sound, rw [nat.iterate₀ (frobenius_one _ _), pow_zero] },
id └─────┘ └──────────┘ └───────────┘ └──────┘
src └──────────────┘└────┘└─────┘└┘└──┘└──────────┘┴ └───────────┘└─────┘└──────┘└┘┴
typ └──────────────┘└────┘└─────┘└┘└──┘└──────────┘┴ └───────────┘└─────┘└──────┘└┘┴
doc └──────────────┘└────┘ └┘└──┘ ┴ └─────┘ └┘┴
txt └──────────────┘└────┘ └┘└──┘ ┴ └─────┘ └┘┴
par └──────────────┘└────┘ └┘└──┘ ┴ └─────┘ └┘┴
pid └───────┘┴└──────┘ └────┘ ┴ └─────┘ └─┘
st ────────────────┘└────────────┘└────────────────────────────────────┘└────────┘┴┴└┘└
222 case nat.succ {
src └───────────────
typ └───────────────
doc └───────────────
txt └───────────────
par └───────────────
pid └───────┘┴└─
st ──────────────────
223 rw [pow_succ, ih],
id └──────┘ └┘
src ───┘└──┘└──────┘└┘ ┴└─
typ ───┘└──┘└──────┘└┘└┘┴└─
doc ───┘└──┘ └┘ ┴└─
txt ───┘└──┘ └┘ ┴└─
par ───┘└──┘ └┘ ┴└─
pid ───────┘ └┘ └──
st ───────────────┘└──┘┴└─
224 symmetry,
src ───┘└──────┘└─
typ ───┘└──────┘└─
doc ───┘└──────┘└─
txt ───┘└──────┘└─
par ───┘└──────┘└─
pid ──────────────
st ───────────┘└─
225 apply r.sound,
id └─────┘
src ───┘└────┘└─────┘└─
typ ───┘└────┘└─────┘└─
doc ───┘└────┘ └─
txt ───┘└────┘ └─
par ───┘└────┘ └─
pid ─────────┘ └─
st ────────────────┘└─
226 simp only [pow_succ, nat.iterate₂ (frobenius_mul _ _)]
id └──────┘ └──────────┘ └───────────┘
src ───┘└─────────┘└──────┘└┘└──────────┘┴ └───────────┘└──────
typ ───┘└─────────┘└──────┘└┘└──────────┘┴ └───────────┘└──────
doc ───┘└─────────┘ └┘ ┴ └──────
txt ───┘└─────────┘ └┘ ┴ └──────
par ───┘└─────────┘ └┘ ┴ └──────
pid ──────────────┘ └┘ ┴ └──────
st ───────────────────────────────────────────────────────────
227 }
src ─┘└┘
typ ─┘└┘
doc ─┘└┘
txt ─┘└┘
par ─┘└┘
pid ──┘┴
st ─┘┴┴
228 end
st └─┘
229
230 def frobenius_equiv [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] :
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
doc └───────┘ └────┘
231 perfect_closure α p ≃ perfect_closure α p :=
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ ┴ └─────────────┘
232 { to_fun := frobenius (perfect_closure α p) p,
id └───────┘ └─────────────┘ ┴ ┴ ┴
src └───────┘ └─────────────┘
typ └───────┘ └─────────────┘ ┴ ┴ ┴
doc └───────┘ └─────────────┘
233 inv_fun := λ e, quot.lift_on e (λ x, quot.mk (r α p) (x.1 + 1, x.2)) (λ x y H,
id ┴ └──────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴ ┴
src └──────────┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └──────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴ ┴
234 match x, y, H with
id ┴ ┴ ┴
typ ┴ ┴ ┴
235 | _, _, r.intro _ n x := quot.sound (r.intro _ _ _)
id └─────┘ └────────┘ └─────┘
src └─────┘ └────────┘ └─────┘
typ └─────┘ └────────┘ └─────┘
236 end),
237 left_inv := λ e, quot.induction_on e (λ ⟨m, x⟩, by rw frobenius_mk;
id ┴ └───────────────┘ ┴ ┴ └──────────┘
src └───────────────┘ └─┘└──────────┘
typ ┴ └───────────────┘ ┴ ┴ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └─────────────────
238 symmetry; apply quot.sound; apply r.intro),
id └────────┘ └─────┘
src └──────┘ └────┘└────────┘ └────┘└─────┘
typ └──────┘ └────┘└────────┘ └────┘└─────┘
doc └──────┘ └────┘ └────┘
txt └──────┘ └────┘ └────┘
par └──────┘ └────┘ └────┘
pid ┴ ┴
st ────────────────────────────────────────────┘
239 right_inv := λ e, quot.induction_on e (λ ⟨m, x⟩, by rw frobenius_mk;
id ┴ └───────────────┘ ┴ ┴ └──────────┘
src └───────────────┘ └─┘└──────────┘
typ ┴ └───────────────┘ ┴ ┴ └─┘└──────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └─────────────────
240 symmetry; apply quot.sound; apply r.intro) }
id └────────┘ └─────┘
src └──────┘ └────┘└────────┘ └────┘└─────┘
typ └──────┘ └────┘└────────┘ └────┘└─────┘
doc └──────┘ └────┘ └────┘
txt └──────┘ └────┘ └────┘
par └──────┘ └────┘ └────┘
pid ┴ ┴
st ────────────────────────────────────────────┘
241
242 theorem frobenius_equiv_apply [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] {x : perfect_closure α p} :
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────────────┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ └─────────────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────────────┘ ┴ ┴
doc └───────┘ └────┘ └─────────────┘
243 frobenius_equiv α p x = frobenius _ p x :=
id └─────────────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
src └─────────────┘ ┴ └───────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘
244 rfl
id └─┘
src └─┘
typ └─┘
245
246 theorem nat_cast [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (n x : ℕ) :
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ ┴
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴
doc └───────┘ └────┘
247 (x : perfect_closure α p) = quot.mk (r α p) (n, x) :=
id ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴
src └─────────────┘ ┴ ┴ ┴
typ ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴┴ ┴
doc └─────────────┘
248 begin
st └─────
249 induction n with n ih,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
250 { induction x with x ih, {refl},
id ┴
src └────────┘ └────────┘ └──┘
typ └────────┘┴└────────┘ └──┘
doc └────────┘ └────────┘ └──┘
txt └────────┘ └────────┘ └──┘
par └────────┘ └────────┘ └──┘
pid ┴ ┴└───────┘
st ───┘└───────────────────┘└─────┘└┘└
251 rw [nat.cast_succ, nat.cast_succ, ih], refl },
id └───────────┘ └───────────┘ └┘
src └──┘└───────────┘└┘└───────────┘└┘ ┴ └───┘
typ └──┘└───────────┘└┘└───────────┘└┘└┘┴ └───┘
doc └──┘ └┘ └┘ ┴ └───┘
txt └──┘ └┘ └┘ ┴ └───┘
par └──┘ └┘ └┘ ┴ └───┘
pid └┘ └┘ └┘ ┴ ┴
st ────────────────────┘└─────────────┘└──┘┴└─────┘└┘└
252 rw ih, apply quot.sound,
id └┘ └────────┘
src └─┘ └────┘└────────┘
typ └─┘└┘ └────┘└────────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ ┴
st ──────┘└────────────────┘└─
253 conv {congr, skip, skip, rw ← frobenius_nat_cast α p x},
id └────────────────┘ ┴ ┴ ┴
src └────┘└───┘└┘└──┘└┘└──┘└┘└───┘└────────────────┘┴ ┴ ┴ ┴
typ └────┘└───┘└┘└──┘└┘└──┘└┘└───┘└────────────────┘┴┴┴┴┴┴┴
txt └────┘└───┘└┘└──┘└┘└──┘└┘└───┘ ┴ ┴ ┴ ┴
par └────┘└───┘└┘└──┘└┘└──┘└┘└───┘ ┴ ┴ ┴ ┴
pid ┴└───────────────────────┘ ┴ ┴ ┴ ┴
st ───────┘└───┘└────┘└────┘└─────────────────────────────┘└┘└
254 apply r.intro
id └─────┘
src └────┘└─────┘┴
typ └────┘└─────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────┘
255 end
st └─┘
256
257 theorem int_cast [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (x : ℤ) :
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ ┴
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴
doc └───────┘ └────┘
258 (x : perfect_closure α p) = quot.mk (r α p) (0, x) :=
id ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴
typ ┴ └─────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
259 by induction x; simp only [int.cast_of_nat, int.cast_neg_succ_of_nat, nat_cast α p 0]; refl
id ┴ └─────────────┘ └──────────────────────┘ └──────┘ ┴ ┴
src └────────┘ └─────────┘└─────────────┘└┘└──────────────────────┘└┘└──────┘┴ ┴ └─┘ └────
typ └────────┘┴ └─────────┘└─────────────┘└┘└──────────────────────┘└┘└──────┘┴┴┴┴└─┘ └────
doc └────────┘ └─────────┘ └┘ └┘ ┴ ┴ └─┘ └────
txt └────────┘ └─────────┘ └┘ └┘ ┴ ┴ └─┘ └────
par └────────┘ └─────────┘ └┘ └┘ ┴ ┴ └─┘ └────
pid ┴ ┴└──┘└┘ └┘ └┘ ┴ ┴ └─┘ └
st └─────────────────────────────────────────────────────────────────────────────────────────
260
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
261 theorem nat_cast_eq_iff [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] (x y : ℕ) :
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ ┴
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴
doc └───────┘ └────┘
262 (x : perfect_closure α p) = y ↔ (x : α) = y :=
id ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴
typ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
263 begin
st └─────
264 split; intro H,
src └───┘ └─────┘
typ └───┘ └─────┘
doc └───┘ └─────┘
txt └───┘ └─────┘
par └───┘ └─────┘
pid └┘
st ───────────────┘└─
265 { rw [nat_cast α p 0, nat_cast α p 0, eq_iff'] at H,
id └──────┘ ┴ ┴ └──────┘ ┴ ┴ └─────┘
src └──┘└──────┘┴ ┴ └──┘└──────┘┴ ┴ └──┘└─────┘└────┘
typ └──┘└──────┘┴┴┴┴└──┘└──────┘┴┴┴┴└──┘└─────┘└────┘
doc └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └────┘
txt └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └────┘
par └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └────┘
pid └┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴└───┘
st ───┘└───────────────┘└──────────────┘└────────┘┴└───┘└─
266 cases H with z H,
id ┴
src └────┘ └───────┘
typ └────┘┴└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ───────────────────┘└─
267 simpa only [zero_add, nat.iterate₀ (frobenius_nat_cast α p _)] using H },
id └──────┘ └──────────┘ └────────────────┘ ┴ ┴ ┴
src └──────────┘└──────┘└┘└──────────┘┴ └────────────────┘┴ ┴ └─────────┘ ┴
typ └──────────┘└──────┘└┘└──────────┘┴ └────────────────┘┴┴┴┴└─────────┘┴┴
doc └──────────┘ └┘ ┴ ┴ ┴ └─────────┘ ┴
txt └──────────┘ └┘ ┴ ┴ ┴ └─────────┘ ┴
par └──────────┘ └┘ ┴ ┴ ┴ └─────────┘ ┴
pid ┴└──┘└┘ └┘ ┴ ┴ ┴ └──┘┴└────┘ ┴
st ──────────────────────────────────────────────────────────────────────────┘└┘└
268 rw [nat_cast α p 0, nat_cast α p 0, H]
id └──────┘ ┴ ┴ └──────┘ ┴ ┴ ┴
src └──┘└──────┘┴ ┴ └──┘└──────┘┴ ┴ └──┘ └┘
typ └──┘└──────┘┴┴┴┴└──┘└──────┘┴┴┴┴└──┘┴└┘
doc └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘
txt └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘
par └──┘ ┴ ┴ └──┘ ┴ ┴ └──┘ └┘
pid └┘ ┴ ┴ └──┘ ┴ ┴ └──┘ ┴┴
st ──────────────────┘└──────────────┘└──┘┴┴
269 end
st └─┘
270
271 instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : char_p (perfect_closure α p) p :=
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └────┘ └─────────────┘ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ └────┘ └─────────────┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └────┘ └─────────────┘ ┴ ┴ ┴
doc └───────┘ └────┘ └────┘ └─────────────┘
272 begin
st └─────
273 constructor, intro x, rw ← char_p.cast_eq_zero_iff α,
id └─────────────────────┘ ┴
src └─────────┘ └─────┘ └───┘└─────────────────────┘┴
typ └─────────┘ └─────┘ └───┘└─────────────────────┘┴┴
doc └─────────┘ └─────┘ └───┘ ┴
txt └─────────┘ └─────┘ └───┘ ┴
par └─────────┘ └─────┘ └───┘ ┴
pid └┘ └─┘ ┴
st ────────────┘└───────┘└──────────────────────────────┘└─
274 rw [← nat.cast_zero, nat_cast_eq_iff, nat.cast_zero]
id └───────────┘ └─────────────┘ └───────────┘
src └────┘└───────────┘└┘└─────────────┘└┘└───────────┘└┘
typ └────┘└───────────┘└┘└─────────────┘└┘└───────────┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid └──┘ └┘ └┘ ┴┴
st ────────────────────┘└───────────────┘└─────────────┘┴┴
275 end
st └─┘
276
277 instance [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] : perfect_field (perfect_closure α p) p :=
id └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ └─────────────┘ ┴ ┴ ┴
src └────────────┘ ┴ └───────┘ └────┘ └───────────┘ └─────────────┘
typ └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────────┘ └─────────────┘ ┴ ┴ ┴
doc └───────┘ └────┘ └───────────┘ └─────────────┘
278 { pth_root := (frobenius_equiv α p).symm,
id └─────────────┘ ┴ ┴ └──┘
src └─────────────┘ └──┘
typ └─────────────┘ ┴ ┴ └──┘
279 frobenius_pth_root := (frobenius_equiv α p).apply_symm_apply }
id └─────────────┘ ┴ ┴ └──────────────┘
src └─────────────┘ └──────────────┘
typ └─────────────┘ ┴ ┴ └──────────────┘
280
281 def of [monoid α] (p : ℕ) (x : α) : perfect_closure α p :=
id └────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └────┘ ┴ └─────────────┘
typ └────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘
282 quot.mk _ (0, x)
id └─────┘ ┴ ┴
src ┴
typ └─────┘ ┴ ┴
283
284 instance [comm_ring α] (p : ℕ) [nat.prime p] [char_p α p] : is_ring_hom (of α p) :=
id └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────────┘ └┘ ┴ ┴
src └───────┘ ┴ └───────┘ └────┘ └─────────┘ └┘
typ └───────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ └─────────┘ └┘ ┴ ┴
doc └───────┘ └────┘ └─────────┘
285 { map_one := rfl,
id └─┘
src └─┘
typ └─┘
286 map_mul := λ x y, rfl,
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
287 map_add := λ x y, rfl }
id ┴ ┴ └─┘
src └─┘
typ ┴ ┴ └─┘
288
289 theorem eq_pth_root [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p] (m : ℕ) (x : α) :
id └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴ ┴
src └────────────┘ ┴ └───────┘ └────┘ ┴
typ └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴ ┴ ┴
doc └───────┘ └────┘
290 quot.mk (r α p) (m, x) = (perfect_field.pth_root p^[m] (of α p x) : perfect_closure α p) :=
id └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └────────────────────┘ ┴└┘┴┴ └┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src ┴ ┴ ┴ └────────────────────┘ └┘ ┴ └┘ └─────────────┘
typ └─────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ └────────────────────┘ ┴└┘┴┴ └┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘
291 begin
st └─────
292 unfold of,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └─┘
st ──────────┘└─
293 induction m with m ih, {refl},
id ┴
src └────────┘ └────────┘ └──┘
typ └────────┘┴└────────┘ └──┘
doc └────────┘ └────────┘ └──┘
txt └────────┘ └────────┘ └──┘
par └────────┘ └────────┘ └──┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─────┘└┘└
294 rw [nat.iterate_succ', ← ih]; refl
id └───────────────┘ └┘
src └──┘└───────────────┘└──┘ ┴ └───┘
typ └──┘└───────────────┘└──┘└┘┴ └───┘
doc └──┘ └──┘ ┴ └───┘
txt └──┘ └──┘ ┴ └───┘
par └──┘ └──┘ ┴ └───┘
pid └┘ └──┘ ┴ ┴
st ──────────────────────┘└────┘┴└─────┘
295 end
st └─┘
296
297 def UMP [discrete_field α] (p : ℕ) [nat.prime p] [char_p α p]
id └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
src └────────────┘ ┴ └───────┘ └────┘
typ └────────────┘ ┴ ┴ └───────┘ ┴ └────┘ ┴ ┴
doc └───────┘ └────┘
298 (β : Type v) [discrete_field β] [char_p β p] [perfect_field β p] :
id └────────────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴
src └────────────┘ └────┘ └───────────┘
typ └────────────┘ ┴ └────┘ ┴ ┴ └───────────┘ ┴ ┴
doc └────┘ └───────────┘
299 { f : α → β // is_ring_hom f } ≃ { f : perfect_closure α p → β // is_ring_hom f } :=
id ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
src ┴ └─────────┘ ┴ ┴ └─────────────┘ └─────────┘
typ ┴ ┴ ┴ ┴ └─────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ └─────────┘ ┴
doc └─────────┘ ┴ └─────────────┘ └─────────┘
300 { to_fun := λ f, ⟨λ e, quot.lift_on e (λ x, perfect_field.pth_root p^[x.1] (f.1 x.2))
id ┴ ┴ └──────────┘ ┴ ┴ └────────────────────┘ ┴└┘┴┴ ┴ ┴┴ ┴┴
src └──────────┘ └────────────────────┘ └┘ ┴ ┴ ┴ ┴
typ ┴ ┴ └──────────┘ ┴ ┴ └────────────────────┘ ┴└┘┴┴ ┴ ┴┴ ┴┴
301 (λ x y H, match x, y, H with | _, _, r.intro _ n x := by letI := f.2;
id ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ └──────┘ └┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ └──────┘┴└┘
doc └──────┘ └┘
txt └──────┘ └┘
par └──────┘ └┘
pid ┴└─┘ └┘
st └─────────────
302 simp only [is_monoid_hom.map_frobenius f.1, nat.iterate_succ, pth_root_frobenius]
id └─────────────────────────┘ ┴ └──────────────┘ └────────────────┘
src └─────────┘└─────────────────────────┘┴ └──┘└──────────────┘└┘└────────────────┘└─
typ └─────────┘└─────────────────────────┘┴┴└──┘└──────────────┘└┘└────────────────┘└─
doc └─────────┘ ┴ └──┘ └┘ └─
txt └─────────┘ ┴ └──┘ └┘ └─
par └─────────┘ ┴ └──┘ └┘ └─
pid ┴└──┘└┘ ┴ └──┘ └┘ ┴└
st ──────────────────────────────────────────────────────────────────────────────────────────
303 end),
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘
304 show f.1 1 = 1, from f.2.1,
id ┴┴ ┴ ┴┴ ┴
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴┴ ┴
305 λ j k, quot.induction_on j $ λ ⟨m, x⟩, quot.induction_on k $ λ ⟨n, y⟩,
id ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
306 show (perfect_field.pth_root p^[_] _) = (perfect_field.pth_root p^[_] _) * (perfect_field.pth_root p^[_] _),
id └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴
src └────────────────────┘ └┘ ┴ ┴ └────────────────────┘ └┘ ┴ ┴ └────────────────────┘ └┘ ┴
typ └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴
307 by letI := f.2; simp only [is_ring_hom.map_mul f.1, (nat.iterate₁ (λ x, (is_monoid_hom.map_frobenius f.1 p x).symm)).symm,
id ┴ └─────────────────┘ ┴ └──────────┘ └─────────────────────────┘ ┴ ┴
src └──────┘ └┘ └─────────┘└─────────────────┘┴ └──┘ └──────────┘┴ └──┘ └─────────────────────────┘┴ └─┘ ┴ └──────────────
typ └──────┘┴└┘ └─────────┘└─────────────────┘┴┴└──┘ └──────────┘┴ └──┘ └─────────────────────────┘┴┴└─┘┴┴ └──────────────
doc └──────┘ └┘ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
txt └──────┘ └┘ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
par └──────┘ └┘ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
pid ┴└─┘ └┘ ┴└──┘└┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
st └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
308 @nat.iterate₂ β _ (*) (λ x y, is_ring_hom.map_mul (perfect_field.pth_root p))];
id └──────────┘ ┴ ┴ └─────────────────┘ └────────────────────┘ ┴
src ─────────┘ └──────────┘┴ └─┘┴└─┘ └────┘└─────────────────┘┴ └────────────────────┘┴ └─┘
typ ─────────┘ └──────────┘┴┴└─┘┴└─┘ └────┘└─────────────────┘┴ └────────────────────┘┴┴└─┘
doc ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
txt ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
par ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
pid ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
st ──────────────────────────────────────────────────────────────────────────────────────────
309 rw [nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p),
id └─────────────┘ └────────────────┘ └────────────────┘ ┴ ┴
src └──┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴ ┴ └──
typ └──┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴┴┴┴└──
doc └──┘ └┘ ┴ ┴ ┴ └──
txt └──┘ └┘ ┴ ┴ ┴ └──
par └──┘ └┘ ┴ ┴ ┴ └──
pid └┘ └┘ ┴ ┴ ┴ └──
st ───────────┘└─────────────┘└───────────────────────────────────────────┘└─
310 add_comm, nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p)],
id └──────┘ └─────────────┘ └────────────────┘ └────────────────┘ ┴ ┴
src ─────────┘└──────┘└┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴ ┴ └┘
typ ─────────┘└──────┘└┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴┴┴┴└┘
doc ─────────┘ └┘ └┘ ┴ ┴ ┴ └┘
txt ─────────┘ └┘ └┘ ┴ ┴ ┴ └┘
par ─────────┘ └┘ └┘ ┴ ┴ ┴ └┘
pid ─────────┘ └┘ └┘ ┴ ┴ ┴ └┘
st ─────────────────┘└───────────────┘└───────────────────────────────────────────┘┴
311 λ j k, quot.induction_on j $ λ ⟨m, x⟩, quot.induction_on k $ λ ⟨n, y⟩,
id ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
src └───────────────┘ └───────────────┘
typ ┴ ┴ └───────────────┘ ┴ ┴ └───────────────┘ ┴ ┴
312 show (perfect_field.pth_root p^[_] _) = (perfect_field.pth_root p^[_] _) + (perfect_field.pth_root p^[_] _),
id └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴
src └────────────────────┘ └┘ ┴ ┴ └────────────────────┘ └┘ ┴ ┴ └────────────────────┘ └┘ ┴
typ └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴ ┴ └────────────────────┘ ┴└┘ ┴
313 by letI := f.2; simp only [is_ring_hom.map_add f.1, (nat.iterate₁ (λ x, (is_monoid_hom.map_frobenius f.1 p x).symm)).symm,
id ┴ └─────────────────┘ ┴ └──────────┘ └─────────────────────────┘ ┴ ┴
src └──────┘ └┘ └─────────┘└─────────────────┘┴ └──┘ └──────────┘┴ └──┘ └─────────────────────────┘┴ └─┘ ┴ └──────────────
typ └──────┘┴└┘ └─────────┘└─────────────────┘┴┴└──┘ └──────────┘┴ └──┘ └─────────────────────────┘┴┴└─┘┴┴ └──────────────
doc └──────┘ └┘ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
txt └──────┘ └┘ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
par └──────┘ └┘ └─────────┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
pid ┴└─┘ └┘ ┴└──┘└┘ ┴ └──┘ ┴ └──┘ ┴ └─┘ ┴ └──────────────
st └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
314 @nat.iterate₂ β _ (+) (λ x y, is_ring_hom.map_add (perfect_field.pth_root p))];
id └──────────┘ ┴ ┴ └─────────────────┘ └────────────────────┘ ┴
src ─────────┘ └──────────┘┴ └─┘┴└─┘ └────┘└─────────────────┘┴ └────────────────────┘┴ └─┘
typ ─────────┘ └──────────┘┴┴└─┘┴└─┘ └────┘└─────────────────┘┴ └────────────────────┘┴┴└─┘
doc ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
txt ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
par ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
pid ─────────┘ ┴ └─┘ └─┘ └────┘ ┴ ┴ └─┘
st ──────────────────────────────────────────────────────────────────────────────────────────
315 rw [nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p),
id └─────────────┘ └────────────────┘ └────────────────┘ ┴ ┴
src └──┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴ ┴ └──
typ └──┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴┴┴┴└──
doc └──┘ └┘ ┴ ┴ ┴ └──
txt └──┘ └┘ ┴ ┴ ┴ └──
par └──┘ └┘ ┴ ┴ ┴ └──
pid └┘ └┘ ┴ ┴ ┴ └──
st ───────────┘└─────────────┘└───────────────────────────────────────────┘└─
316 add_comm m, nat.iterate_add, nat.iterate_cancel (pth_root_frobenius β p)]⟩,
id └──────┘ ┴ └─────────────┘ └────────────────┘ └────────────────┘ ┴ ┴
src ─────────┘└──────┘┴ └┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴ ┴ └┘
typ ─────────┘└──────┘┴┴└┘└─────────────┘└┘└────────────────┘┴ └────────────────┘┴┴┴┴└┘
doc ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘
txt ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘
par ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘
pid ─────────┘ ┴ └┘ └┘ ┴ ┴ ┴ └┘
st ───────────────────┘└───────────────┘└───────────────────────────────────────────┘┴
317 inv_fun := λ f, ⟨f.1 ∘ of α p, @@is_ring_hom.comp _ _ _ _ _ _ f.2⟩,
id ┴ ┴┴ ┴ └┘ ┴ ┴ └──────────────┘ ┴┴
src ┴ ┴ └┘ └──────────────┘ ┴
typ ┴ ┴┴ ┴ └┘ ┴ ┴ └──────────────┘ ┴┴
doc └──────────────┘
318 left_inv := λ ⟨f, hf⟩, subtype.eq rfl,
id ┴ └────────┘ └─┘
src └────────┘ └─┘
typ ┴ └────────┘ └─┘
319 right_inv := λ ⟨f, hf⟩, subtype.eq $ funext $ λ i, quot.induction_on i $ λ ⟨m, x⟩,
id ┴┴ └────────┘ └────┘ ┴ └───────────────┘ ┴ ┴┴
src └────────┘ └────┘ └───────────────┘
typ ┴┴ └────────┘ └────┘ ┴ └───────────────┘ ┴ ┴┴
320 show perfect_field.pth_root p^[m] (f _) = f _,
id └────────────────────┘ ┴└┘ ┴ ┴
src └────────────────────┘ └┘ ┴ ┴
typ └────────────────────┘ ┴└┘ ┴ ┴
321 by resetI; rw [eq_pth_root, @nat.iterate₁ _ _ _ _ f (λ x:perfect_closure α p, (is_ring_hom.pth_root p f).symm)] }
id └─────────┘ └──────────┘ └─────────────┘ ┴ └──────────────────┘ ┴ ┴
src └────┘ └──┘└─────────┘└┘ └──────────┘└───────┘ ┴ └─┘└─────────────┘┴ ┴ └┘ └──────────────────┘┴ ┴ └───────┘
typ └────┘ └──┘└─────────┘└┘ └──────────┘└───────┘ ┴ └─┘└─────────────┘┴┴┴ └┘ └──────────────────┘┴┴┴┴└───────┘
doc └────┘ └──┘ └┘ └───────┘ ┴ └─┘└─────────────┘┴ ┴ └┘ ┴ ┴ └───────┘
txt └────┘ └──┘ └┘ └───────┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └───────┘
par └────┘ └──┘ └┘ └───────┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └───────┘
pid └┘ └┘ └───────┘ ┴ └─┘ ┴ ┴ └┘ ┴ ┴ └──────┘┴
st └──────────────────────┘└──────────────────────────────────────────────────────────────────────────────────┘┴┴
322
323 end perfect_closure